\begin{tabbing}
$\forall$\=$E$:Type, ${\it dE}$:EqDecider($E$), ${\it dL}$:EqDecider(IdLnk), $V$:(Knd$\rightarrow$Id$\rightarrow$Type), ${\it pred?}$:($E$$\rightarrow$($E$+Unit)),\+
\\[0ex]${\it info}$:($E$$\rightarrow$(Id$\times$Id+(IdLnk$\times$$E$)$\times$Id)), ${\it val}$:($e$:$E$$\rightarrow$$V$(kind($e$),loc($e$))),
\\[0ex]$p$:(\=$\forall$$e$:$E$, $l$:IdLnk.\+
\\[0ex]$\exists$${\it e'}$:$E$.
\\[0ex]$\forall$${\it e''}$:$E$.
\\[0ex]rcv?(${\it e''}$)
\\[0ex]$\Rightarrow$ sender(${\it e''}$) $=$ $e$
\\[0ex]$\Rightarrow$ link(${\it e''}$) $=$ $l$
\\[0ex]$\Rightarrow$ ${\it e''}$ $=$ ${\it e'}$ $\vee$ ${\it e''}$ $<$ ${\it e'}$ \& loc(${\it e'}$) $=$ destination($l$) $\in$ Id), $e$:$E$, $l$:IdLnk.
\-\-\\[0ex]SWellFounded($\neg$first($y$) \& $x$ $=$ pred($y$) $\in$ $E$)
\\[0ex]$\Rightarrow$ sends(${\it dE}$;${\it dL}$;${\it pred?}$;${\it info}$;${\it val}$;$p$;$e$;$l$) $\in$ Msg\_sub($l$;$\lambda$$l$,${\it tg}$. $V$(rcv($l$,${\it tg}$),destination($l$))) List
\end{tabbing}